p:FinProbSpace, n:, X, Y:RandomVariable(p;n). X  Y  E(n;X)  E(n;Y) 

latex

Definitions

{x:A| B(x)} , FinProbSpace, , a < b, a  b, r  s, False, A, x:AB(x), RandomVariable(p;n), X  Y, t  T, #$n, x:A. B(x), A  B, Void, P  Q, , s = t, , b, b, , (i = j), x:A  B(x), P & Q, P  Q, Unit, left + right, Outcome, null, i  j , -n, n+m, n - m, x:A.B(x), Top, , type List, S  T, xL. P(x), {i..j}, A c B, , ||as||, i  j < k, null(as), Type, (x  l), x. t(x), l[i], a  j < b. E(j), rv-shift(x;X), E(n;F), , A  B, x,y:A//B(x;y), if b then t else f fi , EquivRel(T;x,y.E(x;y)), tt, qeq(r;s), x,y. t(x;y), f(a), x.A(x), True, T, SqStable(P), cons-seq(x;s)

Lemmas

cons-seq wf, squash wf, true wf, ws-monotone, int seg properties, length wf nat, sq stable from decidable, decidable qle, int-rational, quotient wf, qeq wf2, btrue wf, b-union wf, int nzero wf, expectation wf, rv-shift wf, qsum wf, select wf, int seg wf, l all wf2, qle wf, int inc rationals, l member wf, null wf3, length wf1, top wf, rationals wf, ge wf, nat properties, finite-prob-space wf, nat wf, null-seq wf, p-outcome wf, eqtt to assert, eqff to assert, iff transitivity, assert of bnot, not functionality wrt iff, assert of eq int, eq int wf, bool wf, bnot wf, not wf, assert wf, rv-le wf, random-variable wf, le wf